feat(GreensOpenProblems/64): formalize Ω(p-2) odd infinitude question#4364
Open
Sanexxxx777 wants to merge 1 commit into
Open
feat(GreensOpenProblems/64): formalize Ω(p-2) odd infinitude question#4364Sanexxxx777 wants to merge 1 commit into
Sanexxxx777 wants to merge 1 commit into
Conversation
|
👋 This is an automated welcome message. 🤖 A few friendly reminders while the review gets started:
Thanks again for helping improve Formal Conjectures. |
github-actions
Bot
added
the
green-problems
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
Green's open problem 64: do there exist infinitely many primes p for
which p - 2 has an odd number of prime factors (counted with
multiplicity)? Stated as `answer(sorry) ↔ {p | p.Prime ∧ Odd (Ω (p-2))}.Infinite`.
Adds three decidable `category test` witnesses: 5 and 7 satisfy the
condition (p-2 prime ⇒ Ω = 1 odd), while 11 does not (9 = 3^2, Ω = 2).
Sanexxxx777
force-pushed
the
greens-64-omega-p-minus-2
branch
from
e8332a0 to
dc36cf6
Compare
mo271
reviewed
Jul 5, 2026
mo271
left a comment
mo271
left a comment
Collaborator
There was a problem hiding this comment.
Thanks, LGTM, just two remarks!
Comment on lines
+23
to
+28
|
|
||
| Do there exist infinitely many primes $p$ for which $p - 2$ has an odd number of prime factors, | ||
| counted with multiplicity? | ||
|
|
||
| Writing $\Omega(n)$ for the number of prime factors of $n$ counted with multiplicity, the question | ||
| asks whether the set of primes $p$ with $\Omega(p - 2)$ odd is infinite. |
Collaborator
There was a problem hiding this comment.
Suggested change
| Do there exist infinitely many primes $p$ for which $p - 2$ has an odd number of prime factors, | |
| counted with multiplicity? | |
| Writing $\Omega(n)$ for the number of prime factors of $n$ counted with multiplicity, the question | |
| asks whether the set of primes $p$ with $\Omega(p - 2)$ odd is infinite. |
No need to repeat this here
| rintro ⟨-, hodd⟩ | ||
| rw [show (11 : ℕ) - 2 = 3 ^ 2 by norm_num, cardFactors_apply_prime_pow (by norm_num)] at hodd | ||
| exact (by decide : ¬ Odd 2) hodd | ||
|
|
Collaborator
There was a problem hiding this comment.
Suggested change
| /-- | |
| The same question as `green_64` but with $p - 1$ instead of $p - 2$. | |
| Green notes this is "probably more natural". | |
| -/ | |
| @[category research open, AMS 11] | |
| theorem green_64.variants.p_sub_one : | |
| answer(sorry) ↔ {p : ℕ | p.Prime ∧ Odd (Ω (p - 1))}.Infinite := by | |
| sorry | |
Perhaps a good addition? One could then also show that this is implied by twin_prime (not sure it we really want that as a test statement...)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Formalizes Green's open problem 64:
Statement
where
ΩisArithmeticFunction.cardFactors(number of prime factors with multiplicity). This mirrors the existing twin-prime style infinitude statements in the repo.Test witnesses
Three decidable
category testlemmas keep the definition honest:green_64_mem_five/green_64_mem_seven: 5 and 7 qualify (for these,p - 2is itself prime, soΩ (p - 2) = 1is odd).green_64_not_mem_eleven: 11 does not qualify, since11 - 2 = 9 = 3 ^ 2givesΩ 9 = 2, which is even — showing the condition is non-trivial.Verification
lake build --wfail 'FormalConjectures.GreensOpenProblems.«64»'passes clean (linters as errors).#print axiomson all three test lemmas:[propext, Classical.choice, Quot.sound]only (nosorryAx).Closes #1684.